The Top SE program is a non-accredited course at Masters level fully funded by the government and is operated through a close collaboration between industry and academia at the National Institute of Informatics. The overview and the curriculum design of the whole program are discussed in [5]. We deliver the following five courses on model checking:Model Checking Foundations,Model Checking Applications, Real-time Model checking, Software Model checking, andModelling and verification of concurrent models. These courses focus on efficient use and proper application of model checking tools that use automata theory, specifically SPIN [4], SMV [7], LTSA [6] and FDR. The key learning objectives of the Foundations and Applications courses are to learn how to detect and correct faults in design specifications in UML state machine models. More detailed explanation was presented in [5].
2.4 MPS
MPS runs an in-house curriculum which aims to teach practical techniques of model checking. We especially focus on the practical side of the technology, and thus we put a higher priority on the practical techniques than on the theory in the curriculum. The objective of the curriculum is to give such a skill to engineers so that they can apply model checking to actual software development immediately.
The curriculum consists of the following three courses: the basic course, the application course, and the practice course. In the basic course, temporal logic and state transition systems are explained with lectures and exercises. The appli-cation course and the practice course are mainly composed of laboratory works in which verifications of flow charts and source codes are taught. Especially, in the practice course, the course materials are taken from softwares developed by the course participants themselves. We use NuSMV [7] in our curriculum. In addition, in the application course and the practice course, we use a GUI tool for NuSMV ”Support Software for Model Checking” which was jointly developed by The Kansai Electric Power Co. and MPS. The aim of the tool is to make the hurdle of applying model checking lower as much as possible when it is applied to actual software development, by reducing burdens in using the bare tool.
3 Evaluation and Observation of Questionnaires
In this section, we will summarize the results of questionnaires carried out by four organizations in terms of understandability, usefulness and feasibility. De-tailed results are shown in Appendix, and Table 2 shows their summary.
Questionnaires were taken before we started working on this joint project so that we used different questionnaire forms. However some questions are shared and fundamental by them. We pick from practical issues: the degree of under-standing of the tools and techniques taught, the usefulness of the tools and tech-niques to students’ own problems, and feasibility of the techtech-niques to be used in the industrial context. In summarizing the results of questionnaires we recog-nize necessities for standardizing questionnaires as well as the curriculum, and thus we notice that we will make a common questionnaire form.
Table 2 shows the result of their shared and fundamental questions. Each question has some choices which represent the degree of goodness and badness, and the number of the positive answers among them are only shown, that is, sums of numbers presented in the boldface in Table 3. The understandability, usefulness and feasibility stand for the number of the participants who could understand the contents of each course, the participants who feel that the model
Table 2.Questionnaire Results
Courses Students Understandability Usefulness Feasibility
AIST (elementary) 75 59(79%) 70 (93%) N/A
AIST (intermediate) 24 7 (29%) 24 (100%) 18 (75%)
TOPSE (foundations) 36 22 (61%) N/A 26 (72%)
TOPSE (applications) 7 5 (71%) N/A 5 (71%)
JAIST 61 58 (95%) 54 (89%) 43 (70%)
MPS (in-house training) 13 10 (77%) N/A 10 (77%)
Total 216 161/216 (74%) 148/160 (93%) 102/141 (72%)
checking is useful in their fields, and the participants who feel that the model checking can be practically feasible in their fields respectively.
On understandability, most of the courses mark high scores. the AIST in-termediate course takes lower points since the contents were rather theoretical compared with other courses. In addition, it must be noted that the results ob-tained in the TOPSE are somewhat different from other courses due to the fact that participants of the program come to learn not only model checking courses but also some other courses such as software architecture and requirements en-gineering. Even taking these backgrounds of each course into account, we can observe that model checking is not so difficult for engineers to learn. The scores of the usefulness and the feasibility have also high similarly to the understand-ability. These results show that the Japanese industry has a potential to appreci-ate model checking, and that model checking is accepted as a practical method in Japanese industry.
We would like to quote some notable comments from the free description of the questionnaires. Many of the participants were surprised at the analysis power of the model checking tools as they know that concurrent and non-deterministic behaviour of the systems is very hard to analyze by hand. On the other hand, some participants were curious about how the model checking tools are inte-grated into their own system development processes. Unfortunately, we do not have suitable answers for this comment right now because the software pro-cesses to apply the model checking tools are not established yet. One way to meet this request is that we show successful examples to them. Making such examples for the education is one of our future works.
These results imply that teaching the model checking technologies to the engineers are fruitful. They were convinced of the relevance to learn the usage and application of the tools. On the other hand, they did not feel that to learn the theory of the model checking even though the theory exists behind the tools.
They might be just interested in how the model checking tools are taken into their daily works. However, we still believe that teaching the tools to the engi-neers is important. Though, right now, their interest is the usage of the tools, the interest will be extended to advanced topics like the theory and principle around the tools. The model checking has the limitations in some senses such as state explosion problems and descriptive power. Those limitations would be the mo-tivation to learn technologies which are complement with the model checking and more advanced issues.
In summary, the overall score of feedback from the participants are very positive. We can conclude that our courses are well accepted by our participants.
We hope that both the industries and academia tackle practical problems not only by taking engineering practices but also scientific approaches into their education programs.
4 Future Direction
As described the previous section, our past activities show participants’ interests and their understanding for model checking. Our courses explained in Section 2 have no or a few vacant seats every time, and indeed we have over 200 respon-dents of questionnaires. We can consider that model checking is a noteworthy technology in Japan. It had not been thought that applying model checking to ac-tual software developments was realistic, but questionnaire results show us it is not true now. There are many participants who comment that they want to apply model checking to actual software development with enough knowledges. We can see from the fact that many people in Japanese industry are understanding applicability of model checking and want to introduce it to software develop-ment processes.
On the other hand, appropriately considered education programs are neces-sary to learn model checking. Such programs should include theoretical back-grounds, since model checking is based on mathematics and logics. Moreover they should include how to use tools efficiently and successful examples in which model checking is applied to software development processes, since Japanese industry is sure to want them. But now every educational organization develops curricula and materials in its own purpose. A sufficiently adaptable and tidy curriculum is needed that considers both of industry’s wants about usage and applications, and theories dealt with at appropriate levels.
In the state described above, in order to let model checking spread in in-dustry, it is necessary to prepare an education program for software engineers, working as a reference. As a collaboration with industry and academia, we plan the following projects for the program:
1. making an MCBOK,
2. making a reference curriculum of model checking, and in this financial year, and further
– improving our MCBOK and curriculum by reviews in public, and – making a system to certifying the skill
in future.
Good curricula should be based on wide knowledge and practices in the subject, including theories, applications, and successful examples. These knowl-edge have not been summarized yet, and thus we will make a model checking body of knowledge (MCBOK) at first. The next is to make a curriculum based on the MCBOK. With MCBOK, one can construct various appropriate curric-ular on model checking and teach it as to various needs and requirements in industry. Our curriculum will be for software engineers, and it will be a ref-erence. It will make possible to compare several curricula (including our own ones) strictly, by mapping them to the reference curriculum. It will also make it possible to cooperate in educations or training in model checking among edu-cational organizations. The MCBOK and the reference curriculum will make a skill in model checking clear, and moreover engineers having a skill in model checking will be certified by them.This certification will encourage software en-gineers to learn about model checking, and will contribute to standardization of model checking for industry.
5 Acknowledgments
The Top SE program is fully supported by the Special Coordination Funds for Promoting Science and Technology, Fostering talent in emerging research field by Ministry of Education, Culture, Sports, Science and Technology, Japan.
We thank Hiroki Takamura and Satoru Yoshida for valuable comments.
References
1. ISO/IEC 15408. Information technology - Security techniques - Evaluation criteria for IT security - Part1, Part2 and Part3. ISO/IEC, 2005.
2. IEC 61508.Functional safety of electrical/electronic/programmable electronic safety-related systems. Bureau Central de la Commission Electrotechnique International, 2000.
3. A. Abran, J. W. Moore, P. Bourque, and R. Dupuis.Guide to the Software Engineering Body of Knowledge 2004 Version SWEBOK. IEEE, 2004.
4. G. J. Holzmann. The SPIN model checker: Primer and reference manual. Addison Wesley, 2004.
5. Shinichi Honiden, Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, and Hironori Washizaki. Top se: Educating superarchitects who can apply software engineering tools to practical development in japan. InICSE, pages 708–718. IEEE Computer Society, 2007.
6. J. Magee and J. Kramer.Concurrency: State Models & Java Programs, Second Edition. John Wiley & Sons, 2006.
7. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA, USA, 1993.
8. Jos´e Nuno Oliveira. A survey of formal methods courses in european higher education. In C. Neville Dean and Raymond T. Boute, editors,Teaching Formal Methods, volume 3294 of Lecture Notes in Computer Science, pages 235–248. Springer, 2004.
A Questionnaire in detail
In this section we show detailed informations of our questionnaires(they are summarized in Section 3): concrete questions, concrete choices, results, and the ratios ofpositiveanswers.
In Table 3, AIST(E), AIST(I), TOPSE(F), and TOPSE(A) mean the courses
AIST(elementary), AIST(intermediate), TOPSE(fundamental), and TOPSE(application) respectively. The column marked by (A) means the number of answers, and
ev-ery datum which we regard as a positive answer is presented in the boldface. The column marked by (B) means the ratio of the positive answers to the population.
Notice that the numbers of vacant answers are not shown.
Table 3.Detailed Questionnaire Results
Understandability
Question Choices (A) (B)
AIST(E) How was the course level? too easy/easy 4
appropriate 55
difficult/too difficult 16 59/75 AIST(I) How was the course level? too easy/easy/bit easy 7
bit difficult/difficult/too difficult 16 7/24 TOPSE(F) Could you catch all the contents? yes/mostly yes 22
neither yes nor no 7
mostly no/no 6 22/36
TOPSE(A) Could you catch all the contents? yes/mostly yes 5
neither yes nor no 2
mostly no/no 0 5/7
JAIST How much could you understand? very well/mostly all 58
could follow 1
little/couldn’t understand 2 58/61 MPS How much do you understand? very well/mostly all 10
average 3
little/couldn’t understand 0 10/13 Usefulness
AIST(E) How do you feel about the course? very useful/useful 70
not useful 0 70/75
AIST(I) How do you feel about the course? very useful/useful/bit useful 24 bit useless/useless/very useless 0 24/24
TOPSE(F) (N/A) -
-TOPSE(A) (N/A) -
-JAIST How do you feel about the course? very useful/useful 54
average 2
useless/very useless 5 54/61
MPS (N/A) -
-Feasibility
AIST(E) (N/A) -
-AIST(I) Do you consider applying MC yes/maybe 18
to your job? maybe not/no 1 18/24
TOPSE(F) Can you apply the course to totally yes/mostly yes 5
your job? partially yes 21
partially no/totally no 4 26/36 TOPSE(A) Can you apply the course to totally yes/mostly yes 1
your job? partially yes 4
partially no/totally no 2 5/7
JAIST How do you feel about feasibility? directly feasible/indirectly feasible 43
feasible in future 6
less feasible/not feasible 12 43/61 MPS How do you feel about feasibility? very feasible/maybe feasible 10
not feasible, but significant 2 personally
less feasible/not feasible 1 10/13
A simple refinement-based method for constructing algorithms
Dominique M´ery
LORIA Nancy Universit´e [email protected]
A Introduction
Overview. Event B is supported by the RODIN platform and provides a frame-work for teaching programming methodology based on the famous pre/post-specifications, together with the refinement. We illustrate a methodology based on Event B and the refinement by developing algorithms like for instance com-puting the shortest distances of a graph, sorting an array by insertion, . . . Floyd’s algorithm is redeveloped and we add comments on the complexity of proofs and on the discovery of invariant; it should be considered as an illustration of a tech-nique introduced in a joint paper with D. Cansell[8]. The development is based on a paradigm identifying a non-deterministic event with a procedure call and by introducing control states. We discuss points related to our lectures at differ-ent levels of the university, mainly master. It is also a way to introduce a pattern used for developing sequential structured programs. The complete development of Floyd’s algorithm can be found in the document [14] and we will illustrate our paper with comments of students. The paper will intend to focus on both Formal Method, namely Event B, and, Education and Training, namely Master Degree Lectures.
Progamming methodology. The development of structured programs is car-ried out either using bottom-up techniques, or top-down techniques; we show how refinement and proof can be used to help in the top-down development of structured imperative programs. When a problem is stated, the incremental proof-based methodology of event B[7] starts by stating a very abstract model and further refinements lead to finer-grain event-based models which are used to derive an algorithm[3]. The main idea is to consider eachprocedure callas an abstract event of a model corresponding to the development of the proce-dure; generally, a procedure is specified by a pre/post specification and then the refinement process leads to a set of events, which are finally combined to ob-tain thebody of the procedure. The refinement process can be considered as an unfoldingofcallsstatements under preservation of invariants. It means that the abstraction corresponds to the procedure call and the body is derived using the
refinement process. The refinement process may also use recursive procedures and supports the top-down refinement. The procedure call simulates the abstract event and the refinement guarantees the correctness of the resulting algorithm.
A preliminary version[8] introduces ideas on a case study and provides an ex-tended partial abstract of the current paper.
Proof-based Development. Proof-based development methods[5, 1, 13] in-tegrate formal proof techniques in the development of software systems. The main idea is to start with a very abstract model of the system under develop-ment. Details are gradually added to this first model by building a sequence of more concrete events. The relationship between two successive models in this sequence is that ofrefinement[5, 1]. The essence of the refinement relationship is that it preserves already provedsystem propertiesincluding safety properties and termination. A development gives rise to a number of, so-called,proof obli-gations, which guarantee its correctness. Such proof obligations are discharged by the proof tool using automatic and interactive proof procedures supported by a proof engine[4]. At the most abstract level it is obligatory to describe the static properties of a model’s data by means of an “invariant” predicate. This gives rise to proof obligations relating to the consistency of the model. They are required to ensure that data properties which are claimed to be invariant are preserved by the events of the model. Each refinement step is associated with a further invariant which relates the data of the more concrete model to that of the abstract model and states any additional invariant properties of the (possibly richer) concrete data model. These invariants, so-called gluing invariants are used in the formulation of the refinement proof obligations. The goal of a event B development is to obtain a proved modeland to implement the correctness-by-construction[12] paradigm. Since the development process leads to a large number of proof obligations, the mastering of proof complexity is a crucial is-sue. Even if a proof tool is available, its effective power is limited by classical results over logical theories and we must distribute the complexity of proofs over the components of the current development, e.g. by refinement. Refinement has the potential to decrease the complexity of the proof process whilst allowing for traceability of requirements. The price to pay is to face possibly complex math-ematical theories and difficult proofs. The re-use of developed models and the structuring mechanisms available in B help in decreasing the complexity.
Education and training. The best way to convince your students that formal methods are something good for you, and then for them, is to apply the medicine to yourself. However, I will be provocative and base my teaching method on the famous quastion of the donkey who is not thirsty and the problem is to convince him to drink. According to the classical leitmotiv, we do not give water to a donkey who is not thirsty. Now, you understand that students may be consider
as donkeys and you should warn that donkeys are very strong and very helpful.
If a farmer wants to give water to a donkey, and if the donkey does not want to drink, the best way is to find another donkey who is drinking water, because he enjoys drinking water. The drinking donkey will make the environment full of happiness and the non-drinking donkey will finally drink, because he under-stands that his neighbour is happy and mer(r)y. Now, back to the paper, and we apply the principle to teaching formal methods. The drinking donkey is the au-thor of the paper and the not-drinking donkey is a student. The water is using a formal method Event B based on sets theory and generalized substitution. The main question is to equip workstations with the software supporting Event B, namely RODIN and it is quit easy. First, after some clicks on the web, students can get the RODIN platform. Second, I give lectures with a video projector and students can check themselves that what I am saying and doing is also doable by them.
The teacher should be able to illustrate concepts using the tool that students will use. The use of set theory is very convenient, since it provides another way to model data. Students should model and not only program. The challenge is clearly to teach them how abstract should be a model and to have realistic case studies. If you use a theorem prover, you should be a demonstration of the feasibility of this approach and not only preaching that theorem provers are useful. Using Event B, two concepts emerge during the first lecture: abstraction and refinement. The most difficult question is to state when a model is a good abstraction and what is a model. Now, we have to consider case studies that appear to be tractable and which are sufficiently complex to require a formal development.
We consider case studies which are mainly sequential algorithms, when completely developed. We have improved the expression of the methodology introduced by Cansell and M´ery [8] by formalizing the different step in a global schema or pattern [14]. We introduce the general view of the pattern as it was expressed in [14].
B The modelling framework
This paper is based on concepts of the Event B modelling language developed by J.-R. Abrial[2, 7]; it us the purpose of thos paper to outline the general methodol-ogy we are applying. The ingredients for describing the modelling process based on events and model refinement can be found in [2, 7]. We assume that the goal is to solve a given problem described by a semi-formal mathematical text and we assume that the problem is defined by a precondition and a postcondition[13].
The modelling process starts by identifying the domain of the problem and it
is expressed using the concept of CONTEXT. A CONTEXT P B (see Fig-ure 1) states the theoretical notions required to be able to express the problem statement in a formal way. TheCONTEXTPB declares
– a domainDwhich is the global set of possible values of the current system.
– a list of constantsx, which is specifying the input of the system under devel-opment,P, which is the set of values forxdefining the precondition, andQ, which is a binary relation overDdefining the postcondition of the problem.
– a list of axioms assigns types to constants and adds knowledges to the RODIN environment; for instance, the axiom 5 states that there is always a solutiony, when the input valuexsatisfies the preconditionP.
/ It appears that the set-theoretical notation 1 is well known by french students; they have used notations like sets, relations, bijections . . . The main problem is that they are often willing to program rather than to model. The first exercises helps them to learn the notation and the link between the keyboard and the screen in the RODIN platform. The ECLIPSE-like interface is not a problem for the student who can get the software through the web. Moreover, we maintain a MOODLE chapter for lectures and students can find lectures notes, exercises and archives containing Event B models. On the mathematical and logical concepts, students have lectures on computability and logical the-ories. They have already heard of axioms and theorems; moreover, the sequent calculus [10] is taught by colleagues and the⊢symbol appears to be friendly.
They have not derived many proofs and RODIN provides a very nice interface for deriving theorems from axioms. The cartsian product of two sets is denoted A×B and a member of the set is denoted x 7→ y with x ∈ Aandy ∈ B;
ussually, we use the notation(x, y) instead ofx 7→ y. This point is not a real problem for computer scientists, since they used to learn new languages very often. The cartsianCONTEXTPB is a simple set-theoretical reformulation of the pre-and-post-specification. ,
ACONTEXTmay include a clauseTHEOREMScontaining properties deriv-able in the theory defined by sets, contants and axioms; theorems are discharged using the proof assistant of the tool RODIN. The underlying language is a (typed) set-theoretical language partially given in Table 1. When an expression E is given, a well-definedness condition is generated by the tool; this point al-lows us to check that some side conditions are true. For instance, the expression f(x)generates a condition asx∈dom(f).
/ The well-definedness condition is a crucial issue in computer science.
This pˆoint provides a way to understand the termination of programs. It is also the opportunity to separate the generous programming from the defensive pro-gramming. We can also refered to the programming-by-contract methodology